(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
a__from(X) → cons(mark(X), from(s(X)))
a__after(0, XS) → mark(XS)
a__after(s(N), cons(X, XS)) → a__after(mark(N), mark(XS))
mark(from(X)) → a__from(mark(X))
mark(after(X1, X2)) → a__after(mark(X1), mark(X2))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(s(X)) → s(mark(X))
mark(0) → 0
a__from(X) → from(X)
a__after(X1, X2) → after(X1, X2)
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
a__after(s(N), cons(X, after(s(X3315_3), cons(X15945_3, X25946_3)))) →+ a__after(mark(N), a__after(s(mark(X3315_3)), cons(mark(X15945_3), X25946_3)))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [X25946_3 / after(s(X3315_3), cons(X15945_3, X25946_3))].
The result substitution is [N / mark(X3315_3), X / mark(X15945_3)].
(2) BOUNDS(n^1, INF)
(3) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.
(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
a__from(X) → cons(mark(X), from(s(X)))
a__after(0', XS) → mark(XS)
a__after(s(N), cons(X, XS)) → a__after(mark(N), mark(XS))
mark(from(X)) → a__from(mark(X))
mark(after(X1, X2)) → a__after(mark(X1), mark(X2))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(s(X)) → s(mark(X))
mark(0') → 0'
a__from(X) → from(X)
a__after(X1, X2) → after(X1, X2)
S is empty.
Rewrite Strategy: INNERMOST
(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.
(6) Obligation:
Innermost TRS:
Rules:
a__from(X) → cons(mark(X), from(s(X)))
a__after(0', XS) → mark(XS)
a__after(s(N), cons(X, XS)) → a__after(mark(N), mark(XS))
mark(from(X)) → a__from(mark(X))
mark(after(X1, X2)) → a__after(mark(X1), mark(X2))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(s(X)) → s(mark(X))
mark(0') → 0'
a__from(X) → from(X)
a__after(X1, X2) → after(X1, X2)
Types:
a__from :: s:from:cons:0':after → s:from:cons:0':after
cons :: s:from:cons:0':after → s:from:cons:0':after → s:from:cons:0':after
mark :: s:from:cons:0':after → s:from:cons:0':after
from :: s:from:cons:0':after → s:from:cons:0':after
s :: s:from:cons:0':after → s:from:cons:0':after
a__after :: s:from:cons:0':after → s:from:cons:0':after → s:from:cons:0':after
0' :: s:from:cons:0':after
after :: s:from:cons:0':after → s:from:cons:0':after → s:from:cons:0':after
hole_s:from:cons:0':after1_0 :: s:from:cons:0':after
gen_s:from:cons:0':after2_0 :: Nat → s:from:cons:0':after
(7) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
a__from,
mark,
a__afterThey will be analysed ascendingly in the following order:
a__from = mark
a__from = a__after
mark = a__after
(8) Obligation:
Innermost TRS:
Rules:
a__from(
X) →
cons(
mark(
X),
from(
s(
X)))
a__after(
0',
XS) →
mark(
XS)
a__after(
s(
N),
cons(
X,
XS)) →
a__after(
mark(
N),
mark(
XS))
mark(
from(
X)) →
a__from(
mark(
X))
mark(
after(
X1,
X2)) →
a__after(
mark(
X1),
mark(
X2))
mark(
cons(
X1,
X2)) →
cons(
mark(
X1),
X2)
mark(
s(
X)) →
s(
mark(
X))
mark(
0') →
0'a__from(
X) →
from(
X)
a__after(
X1,
X2) →
after(
X1,
X2)
Types:
a__from :: s:from:cons:0':after → s:from:cons:0':after
cons :: s:from:cons:0':after → s:from:cons:0':after → s:from:cons:0':after
mark :: s:from:cons:0':after → s:from:cons:0':after
from :: s:from:cons:0':after → s:from:cons:0':after
s :: s:from:cons:0':after → s:from:cons:0':after
a__after :: s:from:cons:0':after → s:from:cons:0':after → s:from:cons:0':after
0' :: s:from:cons:0':after
after :: s:from:cons:0':after → s:from:cons:0':after → s:from:cons:0':after
hole_s:from:cons:0':after1_0 :: s:from:cons:0':after
gen_s:from:cons:0':after2_0 :: Nat → s:from:cons:0':after
Generator Equations:
gen_s:from:cons:0':after2_0(0) ⇔ 0'
gen_s:from:cons:0':after2_0(+(x, 1)) ⇔ cons(0', gen_s:from:cons:0':after2_0(x))
The following defined symbols remain to be analysed:
mark, a__from, a__after
They will be analysed ascendingly in the following order:
a__from = mark
a__from = a__after
mark = a__after
(9) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol mark.
(10) Obligation:
Innermost TRS:
Rules:
a__from(
X) →
cons(
mark(
X),
from(
s(
X)))
a__after(
0',
XS) →
mark(
XS)
a__after(
s(
N),
cons(
X,
XS)) →
a__after(
mark(
N),
mark(
XS))
mark(
from(
X)) →
a__from(
mark(
X))
mark(
after(
X1,
X2)) →
a__after(
mark(
X1),
mark(
X2))
mark(
cons(
X1,
X2)) →
cons(
mark(
X1),
X2)
mark(
s(
X)) →
s(
mark(
X))
mark(
0') →
0'a__from(
X) →
from(
X)
a__after(
X1,
X2) →
after(
X1,
X2)
Types:
a__from :: s:from:cons:0':after → s:from:cons:0':after
cons :: s:from:cons:0':after → s:from:cons:0':after → s:from:cons:0':after
mark :: s:from:cons:0':after → s:from:cons:0':after
from :: s:from:cons:0':after → s:from:cons:0':after
s :: s:from:cons:0':after → s:from:cons:0':after
a__after :: s:from:cons:0':after → s:from:cons:0':after → s:from:cons:0':after
0' :: s:from:cons:0':after
after :: s:from:cons:0':after → s:from:cons:0':after → s:from:cons:0':after
hole_s:from:cons:0':after1_0 :: s:from:cons:0':after
gen_s:from:cons:0':after2_0 :: Nat → s:from:cons:0':after
Generator Equations:
gen_s:from:cons:0':after2_0(0) ⇔ 0'
gen_s:from:cons:0':after2_0(+(x, 1)) ⇔ cons(0', gen_s:from:cons:0':after2_0(x))
The following defined symbols remain to be analysed:
a__from, a__after
They will be analysed ascendingly in the following order:
a__from = mark
a__from = a__after
mark = a__after
(11) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol a__from.
(12) Obligation:
Innermost TRS:
Rules:
a__from(
X) →
cons(
mark(
X),
from(
s(
X)))
a__after(
0',
XS) →
mark(
XS)
a__after(
s(
N),
cons(
X,
XS)) →
a__after(
mark(
N),
mark(
XS))
mark(
from(
X)) →
a__from(
mark(
X))
mark(
after(
X1,
X2)) →
a__after(
mark(
X1),
mark(
X2))
mark(
cons(
X1,
X2)) →
cons(
mark(
X1),
X2)
mark(
s(
X)) →
s(
mark(
X))
mark(
0') →
0'a__from(
X) →
from(
X)
a__after(
X1,
X2) →
after(
X1,
X2)
Types:
a__from :: s:from:cons:0':after → s:from:cons:0':after
cons :: s:from:cons:0':after → s:from:cons:0':after → s:from:cons:0':after
mark :: s:from:cons:0':after → s:from:cons:0':after
from :: s:from:cons:0':after → s:from:cons:0':after
s :: s:from:cons:0':after → s:from:cons:0':after
a__after :: s:from:cons:0':after → s:from:cons:0':after → s:from:cons:0':after
0' :: s:from:cons:0':after
after :: s:from:cons:0':after → s:from:cons:0':after → s:from:cons:0':after
hole_s:from:cons:0':after1_0 :: s:from:cons:0':after
gen_s:from:cons:0':after2_0 :: Nat → s:from:cons:0':after
Generator Equations:
gen_s:from:cons:0':after2_0(0) ⇔ 0'
gen_s:from:cons:0':after2_0(+(x, 1)) ⇔ cons(0', gen_s:from:cons:0':after2_0(x))
The following defined symbols remain to be analysed:
a__after
They will be analysed ascendingly in the following order:
a__from = mark
a__from = a__after
mark = a__after
(13) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol a__after.
(14) Obligation:
Innermost TRS:
Rules:
a__from(
X) →
cons(
mark(
X),
from(
s(
X)))
a__after(
0',
XS) →
mark(
XS)
a__after(
s(
N),
cons(
X,
XS)) →
a__after(
mark(
N),
mark(
XS))
mark(
from(
X)) →
a__from(
mark(
X))
mark(
after(
X1,
X2)) →
a__after(
mark(
X1),
mark(
X2))
mark(
cons(
X1,
X2)) →
cons(
mark(
X1),
X2)
mark(
s(
X)) →
s(
mark(
X))
mark(
0') →
0'a__from(
X) →
from(
X)
a__after(
X1,
X2) →
after(
X1,
X2)
Types:
a__from :: s:from:cons:0':after → s:from:cons:0':after
cons :: s:from:cons:0':after → s:from:cons:0':after → s:from:cons:0':after
mark :: s:from:cons:0':after → s:from:cons:0':after
from :: s:from:cons:0':after → s:from:cons:0':after
s :: s:from:cons:0':after → s:from:cons:0':after
a__after :: s:from:cons:0':after → s:from:cons:0':after → s:from:cons:0':after
0' :: s:from:cons:0':after
after :: s:from:cons:0':after → s:from:cons:0':after → s:from:cons:0':after
hole_s:from:cons:0':after1_0 :: s:from:cons:0':after
gen_s:from:cons:0':after2_0 :: Nat → s:from:cons:0':after
Generator Equations:
gen_s:from:cons:0':after2_0(0) ⇔ 0'
gen_s:from:cons:0':after2_0(+(x, 1)) ⇔ cons(0', gen_s:from:cons:0':after2_0(x))
No more defined symbols left to analyse.